(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** Sk -> Ss *)

(* 侧滑角β (sidelip angle) *)
Parameter beta : R.

(* 迎角 α  (angle of attack) *)
Parameter alpha : R.



(* γ  *)
Parameter gamma : R.

(* Sk在飞机对称面转动 μ度 得到S' *)
Definition coordinate_transform_SkSa :  Mat R 3 3 := mkMat_3_3
  1       0           0
  0  (cos gamma) (-sin gamma)
  0  (sin gamma) (cos gamma).

Definition coordinate_transform_SaSs : Mat R 3 3 := mkMat_3_3
  (cos beta)   (-sin beta)   0
  (sin beta)   (cos beta)    0
      0           0          1.

Definition SkToSs :Mat R 3 3 := mkMat_3_3
  (cos beta) (-(cos gamma)*(sin beta)) ((sin gamma)*(sin beta))
  (sin beta) ((cos gamma)*(cos beta))  (-(sin gamma)*(cos beta))
      0      (sin gamma)               (cos gamma).


Lemma SkToSs_eq:
  SkToSs === RMmul coordinate_transform_SaSs coordinate_transform_SkSa.
Proof.
  unfold SkToSs.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal3. ring. f_equal. ring. f_equal. ring. f_equal. ring.
Qed.

